Coherent space

In proof theory, a coherent space (also coherence space) is a concept introduced in the semantic study of linear logic.

Let a set C be given. Two subsets S,T ⊆ C are said to be orthogonal, written S ⊥ T, if S ∩ T is ∅ or a singleton. The dual of a family F ⊆ ℘(C) is the family F ^⊥ of all subsets S ⊆ C orthogonal to every member of F, i.e., such that S ⊥ T for all T ∈ F. A coherent space F over C is a family of C-subsets for which F = (F ^⊥) ^⊥.

In Proofs and Types coherent spaces are called coherence spaces. A footnote explains that although in the French original they were espaces cohérents, the coherence space translation was used because spectral spaces are sometimes called coherent spaces.

Definitions

As defined by Jean-Yves Girard, a coherence space [math]\displaystyle{ \mathcal{A} }[/math] is a collection of sets satisfying down-closure and binary completeness in the following sense:

• Down-closure: all subsets of a set in [math]\displaystyle{ \mathcal A }[/math] remain in [math]\displaystyle{ \mathcal A }[/math]: [math]\displaystyle{ a' \subset a \in \mathcal A \implies a' \in \mathcal A }[/math]
• Binary completeness: for any subset [math]\displaystyle{ M }[/math] of [math]\displaystyle{ \mathcal A }[/math], if the pairwise union of any of its elements is in [math]\displaystyle{ \mathcal A }[/math], then so is the union of all the elements of [math]\displaystyle{ M }[/math]: [math]\displaystyle{ \forall M \subset \mathcal A, \left((\forall a_1, a_2 \in M,\ a_1 \cup a_2 \in \mathcal A) \implies \bigcup M \in \mathcal A\right) }[/math]

The elements of the sets in [math]\displaystyle{ \mathcal A }[/math] are known as tokens, and they are the elements of the set [math]\displaystyle{ |\mathcal A| = \bigcup \mathcal A = \{ \alpha | \{\alpha\} \in \mathcal A \} }[/math].

Coherence spaces correspond one-to-one with (undirected) graphs (in the sense of a bijection from the set of coherence spaces to that of undirected graphs). The graph corresponding to [math]\displaystyle{ \mathcal A }[/math] is called the web of [math]\displaystyle{ \mathcal A }[/math] and is the graph induced a reflexive, symmetric relation [math]\displaystyle{ \sim }[/math] over the token space [math]\displaystyle{ |\mathcal A| }[/math] of [math]\displaystyle{ \mathcal A }[/math] known as coherence modulo [math]\displaystyle{ \mathcal A }[/math] defined as:[math]\displaystyle{ a \sim b \iff \{a, b\} \in \mathcal A }[/math]In the web of [math]\displaystyle{ \mathcal A }[/math], nodes are tokens from [math]\displaystyle{ |\mathcal A| }[/math] and an edge is shared between nodes [math]\displaystyle{ a }[/math] and [math]\displaystyle{ b }[/math] when [math]\displaystyle{ a \sim b }[/math] (i.e. [math]\displaystyle{ \{a, b\} \in \mathcal A }[/math].) This graph is unique for each coherence space, and in particular, elements of [math]\displaystyle{ \mathcal A }[/math] are exactly the cliques of the web of [math]\displaystyle{ \mathcal A }[/math] i.e. the sets of nodes whose elements are pairwise adjacent (share an edge.)

Coherence spaces as types

Coherence spaces can act as an interpretation for types in type theory where points of a type [math]\displaystyle{ \mathcal A }[/math] are points of the coherence space [math]\displaystyle{ \mathcal A }[/math]. This allows for some structure to be discussed on types. For instance, each term [math]\displaystyle{ a }[/math] of a type [math]\displaystyle{ \mathcal A }[/math] can be given a set of finite approximations [math]\displaystyle{ I }[/math] which is in fact, a directed set with the subset relation. With [math]\displaystyle{ a }[/math] being a coherent subset of the token space [math]\displaystyle{ |\mathcal A| }[/math] (i.e. an element of [math]\displaystyle{ \mathcal A }[/math]), any element of [math]\displaystyle{ I }[/math] is a finite subset of [math]\displaystyle{ a }[/math] and therefore also coherent, and we have [math]\displaystyle{ a = \bigcup a_i, a_i \in I. }[/math]

Stable functions

Functions between types [math]\displaystyle{ \mathcal A \to \mathcal B }[/math] are seen as stable functions between coherence spaces. A stable function is defined to be one which respects approximants and satisfies a certain stability axiom. Formally, [math]\displaystyle{ F : \mathcal A \to \mathcal B }[/math] is a stable function when

1. It is monotone with respect to the subset order (respects approximation, categorically, is a functor over the poset [math]\displaystyle{ \mathcal A }[/math]): [math]\displaystyle{ a' \subset a \in \mathcal A \implies F(a') \subset F(a). }[/math]
2. It is continuous (categorically, preserves filtered colimits): [math]\displaystyle{ F(\bigcup_{i\in I}^{\uparrow}a_i)= \bigcup_{i\in I}^\uparrow F(a_i) }[/math] where [math]\displaystyle{ \bigcup_{i\in I}^\uparrow }[/math] is the directed union over [math]\displaystyle{ I }[/math], the set of finite approximants of [math]\displaystyle{ a }[/math].
3. It is stable: [math]\displaystyle{ a_1 \cup a_2 \in \mathcal A \implies F(a_1 \cap a_2) = F(a_1) \cap F(a_2). }[/math] Categorically, this means that it preserves the pullback:
   

Product space

In order to be considered stable, functions of two arguments must satisfy the criterion 3 above in this form: [math]\displaystyle{ a_1 \cup a_2 \in \mathcal A \land b_1 \cup b_2 \in \mathcal B \implies F(a_1 \cap a_2, b_1 \cap b_2) = F(a_1, b_1) \cap F(a_2, b_2) }[/math]which would mean that in addition to stability in each argument alone, the pullback

is preserved with stable functions of two arguments. This leads to the definition of a product space [math]\displaystyle{ \mathcal A\ \&\ \mathcal B }[/math] which makes a bijection between stable binary functions (functions of two arguments) and stable unary functions (one argument) over the product space. The product coherence space is a product in the categorical sense i.e. it satisfies the universal property for products. It is defined by the equations:

• [math]\displaystyle{ | \mathcal A \ \&\ \mathcal B| = |\mathcal A| + |\mathcal B| = (\{1\} \times |\mathcal A|) \cup (\{2\} \times |\mathcal B|) }[/math] (i.e. the set of tokens of [math]\displaystyle{ \mathcal A \ \&\ \mathcal B }[/math] is the coproduct (or disjoint union) of the token sets of [math]\displaystyle{ \mathcal A }[/math] and [math]\displaystyle{ \mathcal B }[/math].
• Tokens from differents sets are always coherent and tokens from the same set are coherent exactly when they are coherent in that set.
  • [math]\displaystyle{ (1, \alpha) \sim_{\mathcal A\ \&\ \mathcal B} (1, \alpha') \iff \alpha \sim_{\mathcal A} \alpha' }[/math]
  • [math]\displaystyle{ (2, \beta) \sim_{\mathcal A\ \&\ \mathcal B} (2, \beta') \iff \beta \sim_{\mathcal B} \beta' }[/math]
  • [math]\displaystyle{ (1, \alpha) \sim_{\mathcal A\ \&\ \mathcal B} (2, \beta), \forall \alpha \in |\mathcal A|, \beta \in |\mathcal B| }[/math]

References

• Girard, J.-Y.; Lafont, Y.; Taylor, P. (1989), Proofs and types, Cambridge University Press, http://www.paultaylor.eu/stable/prot.pdf .
• Girard, J.-Y. (2004), "Between logic and quantic: a tract", in Ehrhard; Girard; Ruet et al., Linear logic in computer science, Cambridge University Press, http://girard.perso.math.cnrs.fr/LLcup.pdf .